This is a visualization of interaction combinators, a model of computation invented by Yves Lafont. It is a universal model of computation, meaning that it can simulate any Turing machine. Interaction combinators are a graph rewriting system. There are only three types of nodes: the constructor node 𝛾, the duplicator node 𝛿, and the eraser node 𝜀. When the principal ports of two nodes are connected, they interact and are replaced by a new graph according to the following rules.

Interaction combinators are interesting as it is a model of computation that is extremely easily parallelizable. Namely, the interaction rules are local and confluent: the rewriting rules only change their immediate neighbourhood, and it doesn't matter in which order they are performed. This means that when, for example, there are 100 places in the graph where principal ports are connected, we can apply the rewriting rules at all of them in parallel at the same time.

Actually interpreting the graphs, or even turning a desired computation into a graph, is not easy. Luckily, there is a way to encode lambda calculus terms as interaction combinator graphs, and vice versa. This allows us to translate the known results about lambda calculus to interaction combinators, and to use the interaction combinator graph rewriting system as a way to evaluate lambda terms.

In the info panel one can view the lambda term corresponding to the current graph, if it is a valid encoding of a lambda term. The lambda terms are represented using de Bruijn indices. For example, when running the "add 7 8" interaction combinator, the lambda term corresponding to the final result will be the church encoding of 15, that is "λλ1(1(1(1(...(10)...))))" with 15 occurrences of 1.

To be precise, the encoding from lambda terms to graphs that we are using is not exactly interaction combinators. If we did the translation exactly to only 𝛾, 𝛿, and 𝜀 the graphs would be absolutely massive. To aleviate this, we introduce labelled duplicator nodes 𝛿i. This way we can translate stratified lambda terms faithfully to modest interaction nets. A term like Ackermann is not stratified and therefor does not work within this translation. Below we have visualized the rewriting rules of the slightly expanded system.

The "Sound (Lambdascope)" presets use the encoding of van Oostrom, van de Looij and Zwitserlood instead, which is correct for every lambda term. Here λ and application become distinct agents (λ and @), sharing uses leveled duplicators 𝛿ₙ, and scope delimiters ▽ₙ mark where each binder's scope begins. The levels are the oracle: as agents commute past binders and delimiters their levels shift, so two duplicators annihilate only when they are genuine twins and commute otherwise. This way terms like Ackermann do work.